Nuprl Lemma : cand_functionality_wrt_iff
11,40
postcript
pdf
a1
,
a2
,
b1
,
b2
:prop{i:l}. (
a1
a2
)
(
b1
b2
)
((
a1
c
b1
)
(
a2
c
b2
))
latex
Definitions
t
T
,
P
Q
,
P
Q
,
A
c
B
,
P
Q
,
P
Q
,
prop{i:l}
,
x
:
A
.
B
(
x
)
Lemmas
iff
wf
origin
a1,a2,b1,b2:prop{i:l}. (a1 
a2) (b1 b2) ((a1 c
b1) (a2 c b2)) a1,a2,b1,b2:prop{i:l}. (a1 a2) (b1 b2) ((a1 c b1) (a2 c b2)) 
T Q Q B Q Qx:A. B(x)